Nuprl Lemma : wellfounded_wf
13,42
postcript
pdf
A
:Type{i},
r
:(
A
A
{i}). WellFnd{i}(
A
;
x
,
y
.
r
(
x
,
y
))
{i'}
latex
Up
well
fnd
,
well
fnd
Definitions
x
(
s
)
,
P
Q
,
x
(
s1
,
s2
)
,
WellFnd{i}(
A
;
x
,
y
.
R
(
x
;
y
))
,
t
T
,
,
x
:
A
.
B
(
x
)
Lemmas
guard
wf
origin
A:Type{i}, r:(A
A
{i}). WellFnd{i}(A;x,y.r(x,y)) 
{i'} A:Type{i}, r:(AA{i}). WellFnd{i}(A;x,y.r(x,y)) {i'} 
Q Tx:A. B(x)